% RA: Relación 02
% OTTER: puzle2.in
% Departamento de Ciencias de la Computación e Inteligencia Artificial
%==============================================================================


%==============================================================================
% Enunciado
%==============================================================================

% Un puzle está compuesto por las siguientes cuatro fichas:
%
%         +----+        +----+        +----+        +----+
%         |\  /|        |\  /|        |\  /|        |\  /|
%         |R\/V|        |V\/R|        |A\/V|        |R\/A|
%         |R/\V|        |V/\R|        |A/\V|        |R/\A|
%         |/  \|        |/  \|        |/  \|        |/  \|
%         +----+        +----+        +----+        +----+
%
% Donde R, V y A representan los colores Rojo, Verde y Azul, respectivamente.
%
% Utilizar OTTER para encontrar todas las maneras posibles de colocar estas
% cuatro fichas en línea, sin repetir, de forma lo colores de los lados
% adyacentes coincidan. En este caso las fichas se pueden girar.

%==============================================================================
% Formalización
%==============================================================================

% Configuración del sistema

% set(auto2).

set(hyper_res).
% set(para_from).
% set(para_into).
assign(max_proofs,-1).

% Este ejercicio es una variante del ejercicio anterior, simplemente hay que
% añadir un campo nuevo al predicado 'ficha' con información sobre la
% orientación de la ficha, y campos al predicado 'posicion' que informen sobre
% las orientaciones de las cuatro fichas.

% Lenguaje:
% ficha(x,y,z,p) - La ficha x en orientación p tiene a la izquierda el color y,
%                  y a la derecha el color z.
% posicion(x1,o1,x2,o2,x3,o3,x4,o4) -
%   Las fichas x1, x2, x3, x4 se pueden colocar en línea con las orientaciones
%   o1, o2, o3, o4, respectivamente, de forma que los colores de los lados
%   adyacentes coinciden.

formula_list(sos).
 all x (x = x).
 all x y (x = y -> y = x).
 all x y z (x = y & y = z -> x = z).

 1 != 2.
 1 != 3.
 1 != 4.
 2 != 3.
 2 != 4.
 3 != 4.

 all x1 x2 z (ficha(z,x1,x2,0) -> ficha(z,x2,x1,1)).

 all x1 x2 x3 x4 y1 y2 y3 y4 y5 o1 o2 o3 o4
  ((ficha(x1,y1,y2,o1) & ficha(x2,y2,y3,o2) &
    ficha(x3,y3,y4,o3) & ficha(x4,y4,y5,o4) &
    x1 != x2 & x1 != x3 & x1 != x4 &
    x2 != x3 & x2 != x4 & x3 != x4) -> posicion(x1,o1,x2,o2,x3,o3,x4,o4)).

 ficha(1,rojo,verde,0).
 ficha(2,verde,rojo,0).
 ficha(3,azul,verde,0).
 ficha(4,rojo,azul,0).
end_of_list.

formula_list(passive).
 all x1 x2 x3 x4 o1 o2 o3 o4
  (posicion(x1,o1,x2,o2,x3,o3,x4,o4) -> $ANS(x1,o1,x2,o2,x3,o3,x4,o4)).
end_of_list.

%==============================================================================
